Community News
List
of News:
Special Issues
Systems Announcements
Fellowships, Awards, Job Announcements
Other Announcements
Constraints Journal: Call for Papers
Special Issue on Abstraction and Automation in Constraint Modeling
Communicated by Alan Frisch
GUEST EDITORS
Alan Frisch, University of York, U.K.
Ian Miguel, University of St. Andrews, U.K.
INTRODUCTION
Constraint
Programming (CP) is a powerful technology that has been successfully
used for tackling a wide range of real-life, complex applications. To
solve a problem with CP it first needs to be modelled by a set of
constraints that must be satisfied by any solution.
Because
formulating such a model, and especially formulating one that is
solvable in practice, is often difficult, CP technology is currently
accessible to only a small number of experts. For CP to be more widely
used by non-experts, more research effort is needed in order to ease
the use of CP technology.
One way of
improving usability is by extending CP technology to enable models to
be formulated at a higher level of abstraction. For instance, support
for set variables (variables whose domain values are
sets) in many constraint languages and solvers has abstracted away from
the low-level details of how the set variable is represented; the user
no longer needs to know these details. However, variables that take
certain other types of values, such as functions and relations, are not
yet supported directly by constraint solvers. In this case, the
abstract variable can be refined into a representation that comprises a
set of more primitive variables and a collection of constraints among
them. In order to avoid forcing the user to perform this step manually,
automated refinement is a key goal.
Automation can
also aid the modelling process by transforming a constraint model into
one that can be solved more effectively. Such transformations
include adding implied constraints, adding symmetry-breaking
constraints, adding constraints to exploit dominances in optimisation
problems, removing propagation-redundant constraints and creating
relaxed versions of the initial problem.
This special issue is devoted to the development and use of abstraction and automation facilities in constraint modelling.
We invite submissions from interested authors in this challenging and important area.
Topics of Interest include, but are not limited to:
- The use of abstraction facilities in formulating models.
- Abstraction in constraint languages.
- Abstract variable domains.
- Abstraction in search control.
- Automated refinement.
- Automated generation of implied constraints.
- Automated generation of symmetry-breaking constraints.
- Automated generation of constraints to exploit dominances.
- Automated generation of relaxations.
Paper Submission
Researchers
are invited to submit original papers that make a significant
contribution to the field to ianm@cs.st-and.ac.uk. (Note that the usual
on-line submission procedure for the Constraints journal will not be
followed initially for the Special Issue). All submissions should be in
.pdf format and follow Constraints Journal guidelines. Papers of at
most 30 journal pages are preferred.
When submitting,
please use the subject "Constraints Special Issue Paper Submission" and
clearly specify the e-mail address and phone number of the
corresponding author. Receipt of papers will be acknowledged.
Submissions will be reviewed by at least two reviewers. All accepted
papers will meet the usual high-quality standards of the Constraints
Journal.
Authors
intending to submit should send an expression of interest (including a
provisional title, list of authors and a few sentences outlining the
topic of the paper) to ianm@cs.st-and.ac.uk by May 1st, 2007.
Important Dates
Expression of interest: May 1st, 2007
Submission of papers: July 1st, 2007
Notification of acceptance: October 1st, 2007 Final versions of accepted papers: Dec 1st, 2007.
Expected publication of the special Issue: 2nd issue of 2008 (Apr 1st).
Important Links
Fellowship Announcement
Kurt Gödel Centenary Prize Fellowship
Communicated by Kurt Gödel Society
The Kurt
Gödel Society is proud to announce the commencement of the
research fellowship prize program in honor and celebration of Kurt
Gödel's 100th birthday.
The research fellowship prize program sponsored by the John Templeton Foundation will offer:
two Ph.D. (pre-doctoral) fellowships of $60,000 US per annum for two
years two post-doctoral fellowships of $ 80,000 US per annum for two
years one senior fellowship of $120,000 US per annum for one year
The purpose of the fellowship is to support original research in mathematical logic, “meta-mathematics,” philosophy
of mathematical logic, and the foundations of mathematics. This
fellowship is to carry forward the legacy of Gödel, whose works exemplify deep insights and breakthrough discoveries in mathematical logic.
The selection will be made based upon an open, international competition. An international Board of Jurors chaired by Professor Harvey Friedman will oversee the process. The finalist papers will be published in a special issue of a premier journal in mathematical logic.
Web:http://kgs.logic.at/goedel-fellowship
Contact: goedel-fellowship@logic.at
Goal and Criteria of Merit:
In pursuit of similar insights and discoveries, we adopt the following criteria of merit for evaluating Fellowship applications:
1. Intellectual
merit, scientific rigor and originality of the submitted paper and work
plan. The paper should combine visionary thinking with academic
excellence.
2. Potential for
significant contribution to basic foundational understanding of logic
and the likelihood for opening new, fruitful lines of inquiry.
3. Impact of the grant on the project and likelihood that the grant will make this new line of research possible.
4. The probability that the pursuit of this line of research is realistic and feasible for the applicant.
5.
Qualifications of the applicants evaluated via CV and recommendation
letters* (*recommendation letters are not required for senior
applications).
Scopes:
Original fellowship proposals from all fields of mathematical logic (such as Computability Theory, Model Theory, Proof Theory, Set Theory),
meta-mathematics, the philosophy of mathematics, and the foundations of mathematics insofar as the research has strong relevance or resemblance to the Gödelian insights and originality.
Preliminary Timeline
December 1, 2006. Announcement
June 15, 2007. Submissions deadline
October 2007. Jury decision due on papers to be published
December 15, 2007. Final versions due
January 2008. Jury decision on winners due
February 2008. Award Ceremony
Mar.-Sept.2008. Commencement of the Fellowships
Journal on Satisfiability, Boolean Modeling, and Computation: Call for Papers
Application of Constraints to Formal Verification
Communicated by Miroslav Velev
We would like to invite you to submit a paper to the special issue of
the Journal on Satisfiability, Boolean Modeling and Computation (JSAT)
on the topic of application of
constraints to formal verification (CFV).
The submission deadline is January 10, 2007.
Topics include, but are not limited to, the following:
- application of constraint solvers to hardware verification;
- application of constraint solvers to software verification;
- dedicated solvers for formal verification problems;
- tuning SAT for formal verification and testing;
- challenging formal verification problems.
If possible, please confirm your intent to submit a paper.
We look forward to your submission,
Miroslav Velev and Joao
Marques-Silva
Editors of the special issue of JSAT on CFV
Software Announcement
Bedwyr: A Proof Search Approach to Model Checking
Communicated by Alwen Tiu
Dear Colleagues,
we would like to
announce the first release of Bedwyr, an extended logic programming
language that allows model checking directly on syntactic expression
possibly containing bindings.
Bedwyr allows
simple and declarative executable specifications of operational
semantics of various programming languages with bindings, type systems
and process calculi, and also supports automatic reasoning for some
simple properties about the specifications. The current distribution of Bedwyr contains a collection of examples involving pi-calculus, including:
- different styles of specifications of operational semantics: late transition system, transition system with abstraction/concretion, polyadic pi calculus, and spi-calculus,
- (open, weak) bisimulation,
- modal logics,
- (symbolic) trace analyses: for checking correspondence assertions, finding attacks on protocols specified in spi-calculus, and finding "separating traces" of processes.
Bedwyr
makes use of a simple form of tabling to support proof search for
inductive and co-inductive specifications (e.g., bisimulation checking
for non-terminating processes).
You will find a general description of Bedwyr below this message. More details can be found on Bedwyr website http://slimmer.gforge.inria.fr/bedwyr/
Sincerely,
Bedwyr developers
Bedwyr is a
programming framework written in OCaml that facilitates natural and
perspicuous presentations of rule oriented computations over syntactic
expressions and that is capable of model checking based reasoning over
such descriptions.
Bedwyr is in
spirit a generalization of logic programming. However, it embodies two
important recent observations about proof search:
- It is possible to formalize both finite success and finite failure in a sequent calculus; proof search in such a proof system can capture both may and must behavior in operational semantics specifications.
- Higher-order abstract syntax can be supported at a logical level by using term-level lambda-binders, the nabla-quantifier, higher-order pattern unification, and explicit substitutions; these features allow reasoning directly on expressions containing bound variables.
The
distribution of Bedwyr includes illustrative applications to the finite
pi-calculus (operational semantics, bisimulation, trace analyses and
modal logics), the spi-calculus (operational semantics), value-passing
CCS, the lambda-calculus, winning strategies for games, and various
other model checking problems. These examples should also show the ease
with which a new rule based system and particular questions about its
properties can be be programmed in Bedwyr. Because of this
characteristic, we believe that the system can be of use to people
interested in the broad area of reasoning about computer systems.
The present distribution of Bedwyr has been developed by the following individuals:
David Baelde & Dale Miller (INRIA & LIX/Ecole Polytechnique)
Andrew Gacek & Gopalan Nadathur (University of Minneapolis)
Alwen Tiu (Australian National University and NICTA).
In the spirit of
an open source project, we welcome contributions in the form of example
applications and also new features from others.
Book Announcement
Handbook of Modal Logic
Communicated by Wiebe va der Hoek
Dear reader,
We are very
pleased to inform you that the above book has now been published.
We hope that you will be as pleased with the final result as we are.
The book is also announced on Elsevier's website. For more information, please go to:
http://books.elsevier.com/uk//elsevier/uk/subindex.asp?maintarget=&isbn=0444516905&country=United+Kingdom&srccode=&ref=CWS1&subcode=&head=&pdf=&basiccode=&txtSearch=&SearchField=&operator=&order=&community=elsevier
Wiebe van der Hoek
PostDoc and Ph.D. Positions
Action Languages and Answer Set Programming
Communicated by Torsten Schaub
Dear colleague,
the research
unit for Systems Biology GoFORSYS offers interdisciplinary PostDoc and
Ph.D. students positions, among others, in the area of Action Languages and Answer Set Programming for Modeling Biological Networks within the KRR group at the University of Potsdam.
The official job advertisement can be found at http://www.goforsys.org/positions.php
For further information about these position please contact:
Prof. Torsten Schaub
Fon +49-331-977-3080/3081
Fax +49-331-977-3122
Email torsten@cs.uni-potsdam.de
Please send your application to the address indicated on the website.
Best regards, -torsten schaub
Ph.D. Positions
Symbolic Computation at RISC-Linz
Communicated by Guenter Landsmann
Symbolic computation is the branch of mathematics and computer science which solves problems on symbolic objects representable on a computer.
RISC-Linz, the Research Institute for Symbolic Computation of the Johannes Kepler University in Linz, Austria, is one of the world’s leading institutions for research and education in this new and promising area. RISC-Linz invites students for its well established Ph.D. program in symbolic computation. For excellent applicants we offer fellowships covering tuition and living expenses.
Applications for studies starting in October should be received by February 15.
For a description of application details and the RISC curriculum, see the web page http://www.risc.uni-linz.ac.at/education/phd/
The RISC Ph.D. Coordinator
phd-coordinator@risc.uni-linz.ac.at
Software Announcement
QBF Certificates: "ozziKs" Now Available
Communicated by Marco Benedetti
When a quantified CSP (QCSP) is claimed to be TRUE by some solver, how can
we verify that such answer is correct?
In a standard CSP, it is just a
matter of checking (in polynomial time) the values assigned to the variables
by the solver against each constraint in the CSP.
In the QCSP
framework things are more complex: As a certificate we need a strategy. A
strategy can be seen as a set of functions - one for each existentially
quantified variable - yielding admissible values for existential variables
as a function of some relevant subset of the universally quantified
ones.
One such strategy is what we can actually check against the set of
constraints to certify its validity.
Also, a strategy is a piece of
information which is itself interesting (provided a "real-world" problem has
been encoded into the underlying QCSP) as it provides an explicit scenario
in which the validity of the quantified set of constraints is
revealed.
For the case of quantified boolean constraints (QBFs), which we
address here, strategies are also called simply certificates.
The
software "ozziKs", whose public availability we publicise here, is the
implementation of an algorithm that:builds a certificate of satisfiability
C(F) - a.k.a. strategy or policy or quantified model - for any given true
Quantified Boolean Formula F for which a suited inference log is available
(at present, only the QBF solver sKizzo produces a suited log); verifies
C(F) against F, thus certifying in a solver-independent way the validity of
F;evaluates user-provided expressions of various kinds over C(F); writes
to file in different formats C(F) and/or the result of the evaluation of the
above mentioned expressions.
A detailed user manual is available here.
Linux, OS-X, and cygwin versions are available for download at http://sKizzo.info.
Marco
Benedetti, PhD
Research Associate
LIFO - University of Orleans
BP
6759 - 45067 Orleans (France)
Tel: +33 (0)2 38 49 47 96
Fax: +33 (0)2
38 41 71 37
E-mail: Marco.Benedetti@univ-orleans.fr
Information & Computation: Call for Papers
Structural Operational Semantics
Communicated by Rob van Glabbeek
AIM:
Structural
operational semantics (SOS) provides a framework for giving operational
semantics to programming and specification languages. A growing number
of programming languages from commercial and academic spheres have been
given usable semantic descriptions by means of structural operational
semantics. Because of its intuitive appeal and flexibility, structural
operational semantics has found considerable application in the study
of the semantics of concurrent processes. Moreover, it is becoming a
viable alternative to denotational semantics in the static analysis of
programs, and in proving compiler correctness.
Recently,
structural operational semantics has been successfully applied as a
formal tool to establish results that hold for classes of process
description languages. This has allowed for the generalisation of
well-known results in the field of process algebra, and for the
development of a meta-theory for process calculi based on the
realization that many of the results in this field only depend upon
general semantic properties of language constructs.
This special
issue aims at documenting state-of-the-art research, new developments
and directions for future investigation in the field of structural
operational semantics. Specific topics of interest include (but are not
limited to):
- programming languages
- process algebras
- higher-order formalisms
- rule formats for operational specifications
- meaning of operational specifications
- comparisons between denotational, axiomatic and operational semantics
- compositionality of modal logics with respect to operational specifications
- congruence with respect to behavioural equivalences
- conservative extensions
- derivation of proof rules from operational specifications
- software tools that automate, or are based on, SOS.
Papers reporting on applications of SOS to software engineering and other areas of computer science are welcome.
This special
issue is an outgrowth of the series of SOS workshops, which started in
2004, and serves in part as a opportunity to publish the full versions
of the best papers presented at SOS 2006. However, papers that were not
presented at SOS 2006 are equally welcome, and all submissions will be
refereed and subjected to the same quality criteria, meeting the
standards of Information and Computation.
Papers submitted
to the special issue must contain original material that has not
previously been published, and parallel submission for publication
elsewhere is not allowed. However, an extended abstract or short
version of the paper may be submitted for presentation at the SOS 2007
workshop, which will take place before the publication of the special
issue.
PAPER SUBMISSION:
We
solicit unpublished papers reporting on original research on the
general theme of SOS. Papers should take the form of a dvi,
postscript or pdf file. We recommend following Elsevier's instructions
at
http://authors.elsevier.com/JournalDetail.html?PubID=622844
and using LaTeX2e with documentclass elsart.
IMPORTANT DATES:
- Submission of tentative title and abstract: 15 December 2006
- Submission of full paper: 15 February 2006
CONTACT and submission address:
sos2006@cs.stanford.edu
EDITORS of this special issue:
Rob van Glabbeek
National ICT Australia
Locked Bag 6016
University of New South Wales
Sydney, NSW 1466
Australia
Peter D. Mosses
Department of Computer Science
Swansea University
Singleton Park
Swansea SA2 8PP
United Kingdom
Software Announcement
Web Interfaces for the ECCE and LOGEN Specializers
Communicated by Michael Leuschel
We would like to announce the availability of web interfaces for two logic program specialization tools: Ecce and Logen.
Ecce
is an automatic online program specialiser for pure Prolog programs
(with built-ins). It takes a pure Prolog program and a query of
interest and then specialises the program for that particular query.
LOGEN
is an offline partial evaluation system for (almost) full Prolog
written using the so called "cogen approach". Basically, the cogen is a
system which:
- based upon an annotated version of the program to be specialised produces a specialised partial evaluator for that program. This partial evaluator is called a generating extension
- the generating extension can be used to specialise the program in a very efficient manner.
The web interfaces for both of these tools are available via:
The
web interfaces allow one to use those systems without installation on a
local machine. They also provide an intuitive access to the various
command-line options. In the case of Logen a graphical way to annotate
the source programs is provided. Both web interfaces were developed
within the EU-funded project ASAP (a web interface to all of ASAP
tools, containing analysis and slicing tools can be found at
http://www.stups.uni-duesseldorf.de/~asap/asap-online-demo/asap.php).
A brief overview of these tools and their web interfaces can be found here:
The choice on which tool to use depends on the particular application.
Ecce
is a fully automatic online specialiser. It is hence easier to use by
inexperienced users, but more difficult to tweak in case specialisation
does not proceed as desired. Ecce uses more refined control techniques and can perform conjunctive partial deduction and slicing, which Logen cannot.
Because of the additional annotation phase, Logen is more difficult to
master by inexperienced users, but the outcome of the specialisation is
easier to tweak and predict. The specialisation phase of Logen is very efficient, with very little overhead compared to ordinary evaluation.
Logen can deal with almost full Prolog, whereas Ecce only deals with
declarative Prolog programs. The latter restricts the range of programs
to which Ecce can be applied, but it also allows Ecce to perform more
powerful optimisations.
Book Announcement
Lectures on the Curry-Howard Isomorphism
Communicated by M.H. Sorensen & P. Urzyczyn
Lectures on the Curry-Howard Isomorphism
Studies in Logic and the Foundations of Mathematics, 149
by Morten Heine Sorensen, Pawel Urzyczyn
ISBN: 0-444-52077-5, 456 pages
This is an entirely rewritten book version of the DIKU lecture notes published online in 1998. The book gives an intruduction to various topics related to the formulas-as-types analogy, in particular:
- Type-free and simply-typed lambda-calculus
- Intuitionistic logic
- Combinatory logic
- Classical logic and control operators
- Sequent calculus
- Dialogue games
- Intuitionistic arithmetic and Godel's system T
- Second-order logic and polymorphism
- Dependent types and pure type systems.
The book contains a large number of exercises, many of these accompanied with extensive hints and solutions.
PostDoc Position
IRISA & INRIA-Rennes
Communicated by Jean-Pierre Talpin
The Espresso
team at INRIA-Rennes (Brittany, France) is seeking for a post-doctorate
to work on the modular verification and validation of GALS software
architectures in avionics.
The Espresso team (http://www.irisa.fr/espresso) develops Polychrony, an embedded software design tool based on a synchronous multi-clocked model of computation.
The topic of the
post-doctorate is the verification globally asynchronous and locally
synchronous software architectures within the open-source design
workbench Topcased (http://www.topcased.org).
More
specifically, the post-doctorate program is interested in the design
and implementation of verification techniques, using synchronous and
asynchronous model-checkers, for the modular verification and
validation of globally asynchronous and locally synchronous software
architectures.
The performance
of model-checkers used and tools designed in the frame of the program
will be assessed by case studies such as a flight guidance system. The
post-doctorate will carry out the definition and implementation of
verification functionalities in the forthcomming Eclipse plugin of the
Polychrony tool, developped by the team.
Preference will
be given to candidates with a background, doctorate study and research
interests in the area of formal methods, verification and
model-checking, and interest in model-driven engineering for embedded
systems.
The position
provides an opportunity to join a large research institute and engage
in research on formal methods for embedded software engineering in
collaboration with an important academic and industrial consortium.
The selected
post-doctorate candidate will be appointed as expert engineer for an
initial and renewable period of 18 monthes. As expert engineer, the
post-doctorate will receive a competitive monthly salary of 2750=80
including social coverages.
Applications,
including a vitae, references and a brief description of research
interests should be sent in reply of the present e-mail.
Awards Announcement
Automated Reasoning Challenge
Communicated by Geoff Sutcliffe
The MPTP
$100 Challenges are sets of classical first-order reasoning problems,
expressed in the TPTP language, to be proved by fully automated
reasoning systems, within specified reasonable resource constraints.
The challenge problems are based on the Mizar Mathematical Library. The
goal of the MPTP challenges is to boost the development of automated
theorem proving and artificial intelligence methods and tools for
reasoning in large theories that involve large numbers of consistently
used concepts. Details of the challenges, including instructions for
entering, are available at ...
http://www.tptp.org/MPTPChallenge/
The winners of
the MPTP challenges will be announced at CADE-21, and will each receive
$100 in real US dollars ... who says there's no money in ATP! Results
on the challenge problems, for publicly available systems, are on the
web page.
If your browser is up to it, the interactive interface is fun to use :-)
Cheers,
Josef (Urban) and Geoff
Software Announcement
ECLiPSe now Open Source and under MPL
Communicated by Joachim Schimpf
The ECLiPSe
Constraint Logic Programming System has recently been open-sourced by
its current owner Cisco Systems, and is available under the terms of an
MPL (Mozilla Public Licence) equivalent.
For those not so familiar with licensing terms, this means essentially:
- the system can now be used by anyone for any purpose, there is no longer a restriction to academic use
- any modification to the source code must be made available under the same licence, i.e. contributed back
- added libraries and application code are not affected by the licence and can, for instance, remain proprietary
We hope that
this step will encourage the wider use of ECLiPSe in both the academic
and commercial world. The new setup will give us better
flexibility to work with contributors from the user base, integrating
more of the interesting work that is being done with ECLiPSe, and
making it available to a wider community.
Cisco itself is going to continue contributing to maintenance and
development, and so is the other current commercial user, CrossCore
Optimization.
The first open-source release is labelled ECLiPSe 5.10 and can be downloaded from either http://www.eclipse-clp.org or from http://www.sourceforge.net/projects/eclipse-clp
The official source repository now also resides on the Sourceforge site.
Enjoy!
The ECLiPSe Team
Constraint: Call for Papers
Constraint Based Methods for Bioinformatics
Communicated by Alessandro Dal Palù
INTRODUCTION
Bioinformatics
is a challenging and
fast growing area of research, which is of utmost importance for our understanding of life. Major contributions to this discipline can provide
significant benefits in medicine,
agriculture, and industry. To pick out
only a few examples, Bioinformatics
tackles problems related to:
- Recognition, analysis, and organization of DNA sequences
- Biological systems simulations (for metabolic or regulatory networks)
- Prediction of the spatial conformations and interactions of biological polymers (e.g., proteins, RNA)
Recently,
these problems have been formalized and
studied using constraints (often over finite
domains or intervals of reals).
Biology is a source of extremely
interesting and computationally expensive tasks, that
can be encoded exploiting the application of
recent and more general techniques of
constraint programming.
As evidence of this trend, various workshops (Constraints and Bioinformatics/Biocomputing at CP97, CP98 and Constraint based
methods for Bioinformatics at ICLP2005
and CP2006) witnessed the interest and the
importance of research in the topic and moreover presented
new developments of constraint technology
(see, e.g., details in http://www.dimi.uniud.it/dovier/WCB06).
We believe that is valuable to gather papers addressing the
application of constraints to biological problems. With this
special issue, we desire to reflect the state of the art of
this field, and thus we seek for papers that report new ideas,
advances and results.
The submission of papers is opened to
anyone who developed ideas and/or obtained results
in the bioinformatics area making use of constraint
programming.
PAPER SUBMISSION
Researchers are invited to submit original or survey papers to all the editors (addresses below). The editors would appreciate
receiving a tentative short abstract
(may be partial) at the beginning
of January. In the first email, please specify the title,
keywords, abstract and the author's
email addresses. Receipt of submissions will be
acknowledged. All final submissions should be in .pdf
format, and must adhere to the Constraints Journal
guidelines http://ai.uwaterloo.ca/~vanbeek/Constraints/Instructions_for_Authors.html
(Note that the usual
on-line submission procedure for the Constraints Journal will not be followed initially for the Special Issue)
We
expect papers no longer than 25 pages, but this is not a
strict constraint. Submissions will be reviewed by at least
two reviewers. All accepted papers will meet the usual high-quality standards of the Constraints Journal.
IMPORTANT DATES
| Abstract Submission: |
January 10th, 2007 |
| Submission Deadline: |
January 31st, 2007 |
| Notification of Acceptance: |
April 30th, 2007 |
| Final Version of Accepted Papers: |
June 30th, 2007 |
GUEST EDITORS
Alessandro Dal Palu', Parma University, Italy.
Email alessandro.dalpalu AT unipr.it
Agostino Dovier, Udine University, Italy.
Email dovier AT dimi.uniud.it
Sebastian Will, Freiburg University, Germany.
Email will AT informatik.uni-freiburg.de
See: http://www.dimi.uniud.it/dovier/WCBSI/